#define rand	pan_rand
#if defined(HAS_CODE) && defined(VERBOSE)
	cpu_printf("Pr: %d Tr: %d\n", II, t->forw);
#endif
	switch (t->forw) {
	default: Uerror("bad forward move");
	case 0:	/* if without executable clauses */
		continue;
	case 1: /* generic 'goto' or 'skip' */
		IfNotBlocked
		_m = 3; goto P999;
	case 2: /* generic 'else' */
		IfNotBlocked
		if (trpt->o_pm&1) continue;
		_m = 3; goto P999;

		 /* PROC q */
	case 3: /* STATE 1 - line 30 "dekker.pml" - [wantq = 1] (0:0:1 - 1) */
		IfNotBlocked
		reached[1][1] = 1;
		(trpt+1)->bup.oval = ((int)now.wantq);
		now.wantq = 1;
#ifdef VAR_RANGES
		logval("wantq", ((int)now.wantq));
#endif
		;
		_m = 3; goto P999; /* 0 */
	case 4: /* STATE 2 - line 32 "dekker.pml" - [(!(wantp))] (0:0:0 - 1) */
		IfNotBlocked
		reached[1][2] = 1;
		if (!( !(((int)now.wantp))))
			continue;
		_m = 3; goto P999; /* 0 */
	case 5: /* STATE 5 - line 35 "dekker.pml" - [((turn==2))] (0:0:0 - 1) */
		IfNotBlocked
		reached[1][5] = 1;
		if (!((((int)now.turn)==2)))
			continue;
		_m = 3; goto P999; /* 0 */
	case 6: /* STATE 6 - line 36 "dekker.pml" - [((turn==1))] (0:0:0 - 1) */
		IfNotBlocked
		reached[1][6] = 1;
		if (!((((int)now.turn)==1)))
			continue;
		_m = 3; goto P999; /* 0 */
	case 7: /* STATE 7 - line 37 "dekker.pml" - [wantq = 0] (0:0:1 - 1) */
		IfNotBlocked
		reached[1][7] = 1;
		(trpt+1)->bup.oval = ((int)now.wantq);
		now.wantq = 0;
#ifdef VAR_RANGES
		logval("wantq", ((int)now.wantq));
#endif
		;
		_m = 3; goto P999; /* 0 */
/* STATE 8 - line 38 "dekker.pml" - [((turn==2))] (0:0 - 1) same as 5 (0:0 - 1) */
/* STATE 9 - line 39 "dekker.pml" - [wantq = 1] (0:0 - 1) same as 3 (0:0 - 1) */
	case 8: /* STATE 15 - line 42 "dekker.pml" - [csq = 1] (0:0:1 - 3) */
		IfNotBlocked
		reached[1][15] = 1;
		(trpt+1)->bup.oval = ((int)now.csq);
		now.csq = 1;
#ifdef VAR_RANGES
		logval("csq", ((int)now.csq));
#endif
		;
		_m = 3; goto P999; /* 0 */
	case 9: /* STATE 16 - line 43 "dekker.pml" - [assert(!((csp&&csq)))] (0:0:0 - 1) */
		IfNotBlocked
		reached[1][16] = 1;
		assert( !((((int)now.csp)&&((int)now.csq))), " !((csp&&csq))", II, tt, t);
		_m = 3; goto P999; /* 0 */
	case 10: /* STATE 17 - line 44 "dekker.pml" - [csq = 0] (0:0:1 - 1) */
		IfNotBlocked
		reached[1][17] = 1;
		(trpt+1)->bup.oval = ((int)now.csq);
		now.csq = 0;
#ifdef VAR_RANGES
		logval("csq", ((int)now.csq));
#endif
		;
		_m = 3; goto P999; /* 0 */
/* STATE 18 - line 45 "dekker.pml" - [wantq = 0] (0:0 - 1) same as 7 (0:0 - 1) */
	case 11: /* STATE 19 - line 46 "dekker.pml" - [turn = 1] (0:0:1 - 1) */
		IfNotBlocked
		reached[1][19] = 1;
		(trpt+1)->bup.oval = ((int)now.turn);
		now.turn = 1;
#ifdef VAR_RANGES
		logval("turn", ((int)now.turn));
#endif
		;
		_m = 3; goto P999; /* 0 */
	case 12: /* STATE 23 - line 48 "dekker.pml" - [-end-] (0:0:0 - 1) */
		IfNotBlocked
		reached[1][23] = 1;
		if (!delproc(1, II)) continue;
		_m = 3; goto P999; /* 0 */

		 /* PROC p */
	case 13: /* STATE 1 - line 8 "dekker.pml" - [wantp = 1] (0:0:1 - 1) */
		IfNotBlocked
		reached[0][1] = 1;
		(trpt+1)->bup.oval = ((int)now.wantp);
		now.wantp = 1;
#ifdef VAR_RANGES
		logval("wantp", ((int)now.wantp));
#endif
		;
		_m = 3; goto P999; /* 0 */
	case 14: /* STATE 2 - line 10 "dekker.pml" - [(!(wantq))] (0:0:0 - 1) */
		IfNotBlocked
		reached[0][2] = 1;
		if (!( !(((int)now.wantq))))
			continue;
		_m = 3; goto P999; /* 0 */
	case 15: /* STATE 5 - line 13 "dekker.pml" - [((turn==1))] (0:0:0 - 1) */
		IfNotBlocked
		reached[0][5] = 1;
		if (!((((int)now.turn)==1)))
			continue;
		_m = 3; goto P999; /* 0 */
	case 16: /* STATE 6 - line 14 "dekker.pml" - [((turn==2))] (0:0:0 - 1) */
		IfNotBlocked
		reached[0][6] = 1;
		if (!((((int)now.turn)==2)))
			continue;
		_m = 3; goto P999; /* 0 */
	case 17: /* STATE 7 - line 15 "dekker.pml" - [wantp = 0] (0:0:1 - 1) */
		IfNotBlocked
		reached[0][7] = 1;
		(trpt+1)->bup.oval = ((int)now.wantp);
		now.wantp = 0;
#ifdef VAR_RANGES
		logval("wantp", ((int)now.wantp));
#endif
		;
		_m = 3; goto P999; /* 0 */
/* STATE 8 - line 16 "dekker.pml" - [((turn==1))] (0:0 - 1) same as 15 (0:0 - 1) */
/* STATE 9 - line 17 "dekker.pml" - [wantp = 1] (0:0 - 1) same as 13 (0:0 - 1) */
	case 18: /* STATE 15 - line 20 "dekker.pml" - [csp = 1] (0:0:1 - 3) */
		IfNotBlocked
		reached[0][15] = 1;
		(trpt+1)->bup.oval = ((int)now.csp);
		now.csp = 1;
#ifdef VAR_RANGES
		logval("csp", ((int)now.csp));
#endif
		;
		_m = 3; goto P999; /* 0 */
	case 19: /* STATE 16 - line 21 "dekker.pml" - [assert(!((csp&&csq)))] (0:0:0 - 1) */
		IfNotBlocked
		reached[0][16] = 1;
		assert( !((((int)now.csp)&&((int)now.csq))), " !((csp&&csq))", II, tt, t);
		_m = 3; goto P999; /* 0 */
	case 20: /* STATE 17 - line 22 "dekker.pml" - [csp = 0] (0:0:1 - 1) */
		IfNotBlocked
		reached[0][17] = 1;
		(trpt+1)->bup.oval = ((int)now.csp);
		now.csp = 0;
#ifdef VAR_RANGES
		logval("csp", ((int)now.csp));
#endif
		;
		_m = 3; goto P999; /* 0 */
/* STATE 18 - line 23 "dekker.pml" - [wantp = 0] (0:0 - 1) same as 17 (0:0 - 1) */
	case 21: /* STATE 19 - line 24 "dekker.pml" - [turn = 2] (0:0:1 - 1) */
		IfNotBlocked
		reached[0][19] = 1;
		(trpt+1)->bup.oval = ((int)now.turn);
		now.turn = 2;
#ifdef VAR_RANGES
		logval("turn", ((int)now.turn));
#endif
		;
		_m = 3; goto P999; /* 0 */
	case 22: /* STATE 23 - line 26 "dekker.pml" - [-end-] (0:0:0 - 1) */
		IfNotBlocked
		reached[0][23] = 1;
		if (!delproc(1, II)) continue;
		_m = 3; goto P999; /* 0 */
	case  _T5:	/* np_ */
		if (!((!(trpt->o_pm&4) && !(trpt->tau&128))))
			continue;
		/* else fall through */
	case  _T2:	/* true */
		_m = 3; goto P999;
#undef rand
	}

